{
"cells": [
{
"cell_type": "markdown",
"id": "388d2860-22b4-4979-a43e-21e8664fbb70",
"metadata": {},
"source": [
"# Parallel composition\n",
"Using the PGC API, you can define your own parallel composition logic. This works similar to PRISM models. We give an example here. We create two MDP models `m1` and `m2`, and then we create the quotient model `q`. They synchronize on the action `r`."
]
},
{
"cell_type": "markdown",
"id": "e18d62d6-b078-4667-82fa-d405d34bdee6",
"metadata": {},
"source": [
"## m1\n",
"`m1` is a simple 2x2 grid model where taking `l` `r` `u` and `d` move to the next tile."
]
},
{
"cell_type": "code",
"execution_count": 1,
"id": "6e028f87-2c33-48db-8543-61c2e2171286",
"metadata": {},
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "9b864c8438744d4ead094fa9cf5e309c",
"version_major": 2,
"version_minor": 0
},
"text/plain": [
"Output()"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"application/javascript": [
"\n",
"function return_id_result(url, id, data) {\n",
" fetch(url, {\n",
" method: 'POST',\n",
" body: JSON.stringify({\n",
" 'id': id,\n",
" 'data': data\n",
" })\n",
" })\n",
" }\n"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"application/javascript": [
"return_id_result('http://127.0.0.1:8889', 'vspMghvbFoLIrcMorJRy', 'test message')"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "5104da1223fe487fa846c7f456a7a9d2",
"version_major": 2,
"version_minor": 0
},
"text/plain": [
"Output()"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"\n",
"\n",
"\n",
" \n",
" Network\n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
"\n"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"from stormvogel import *\n",
"N = 2\n",
"\n",
"ACTION_SEMANTICS = {\n",
" \"l\": (-1, 0),\n",
" \"r\": (1, 0),\n",
" \"u\": (0, -1),\n",
" \"d\": (0, 1) }\n",
"\n",
"def available_actions_m1(s):\n",
" res = []\n",
" if s[0] > 0:\n",
" res.append(\"l\")\n",
" if s[0] < N-1:\n",
" res.append(\"r\")\n",
" if s[1] > 0:\n",
" res.append(\"u\")\n",
" if s[1] < N-1:\n",
" res.append(\"d\")\n",
" return res\n",
"\n",
"def pairwise_plus(t1, t2):\n",
" return (t1[0] + t2[0], t1[1] + t2[1])\n",
"\n",
"def delta_m1(s, a):\n",
" return [(1, pairwise_plus(s, ACTION_SEMANTICS[a]))]\n",
"\n",
"def labels_m1(s):\n",
" return [str(s)]\n",
"\n",
"m1 = pgc.build_pgc(\n",
" initial_state_pgc=(0,0),\n",
" available_actions=available_actions_m1,\n",
" labels=labels_m1,\n",
" delta=delta_m1)\n",
"vis_m1 = show(m1)"
]
},
{
"cell_type": "markdown",
"id": "f2831206-6e13-448a-bf7e-7d6023a64a22",
"metadata": {},
"source": [
"## m2\n",
"`m2` is a model that counts the number of `r` up until two, and has a faulty reset button `c` to reset the counter. It only works in 80% of the cases. It only allows `r` if the count is not already 2."
]
},
{
"cell_type": "code",
"execution_count": 2,
"id": "8a2859df-d33a-43f6-bf15-48e631de30a8",
"metadata": {},
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "2bfa51111629463697092df5a0c2daaf",
"version_major": 2,
"version_minor": 0
},
"text/plain": [
"Output()"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "7a5d442a7aab457faf3593cccd736a14",
"version_major": 2,
"version_minor": 0
},
"text/plain": [
"Output()"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"\n",
"\n",
"\n",
" \n",
" Network\n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
"\n"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"def available_actions_m2(s):\n",
" if s <= 1:\n",
" return [\"r\", \"c\"]\n",
" if s == 2:\n",
" return [\"c\"]\n",
"\n",
"def delta_m2(s, a):\n",
" if s <= 1:\n",
" if \"r\" in a:\n",
" return [(1, s+1)]\n",
" elif s == 0:\n",
" return [(1,0)]\n",
" else:\n",
" return [(.8, 0), (.2, s)]\n",
" else:\n",
" return [(.8, 0), (.2, s)]\n",
"\n",
"def labels_m2(s):\n",
" return [str(s)]\n",
"\n",
"m2 = pgc.build_pgc(\n",
" initial_state_pgc=0,\n",
" available_actions=available_actions_m2,\n",
" labels=labels_m2,\n",
" delta=delta_m2)\n",
"vis_m2 = show(m2)"
]
},
{
"cell_type": "markdown",
"id": "01d2a2bf-07d2-40f3-b22d-ab681054b73b",
"metadata": {},
"source": [
"# Quotient model\n",
"Now we construct the quotient model."
]
},
{
"cell_type": "code",
"execution_count": 3,
"id": "ef023900-dcfd-4906-8bcc-fb6c6555c8ef",
"metadata": {},
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "911b7e80ef1f46feaf3b72b88d919b84",
"version_major": 2,
"version_minor": 0
},
"text/plain": [
"Output()"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "10521771daae4e7ab65cff6f86d04533",
"version_major": 2,
"version_minor": 0
},
"text/plain": [
"Output()"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"\n",
"\n",
"\n",
" \n",
" Network\n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
"\n"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"SYNC = [\"r\"]\n",
"\n",
"def prob_product(branch1, branch2):\n",
" return [(p1 * p2, (r1, r2)) for p1, r1 in branch1 for p2, r2 in branch2]\n",
"\n",
"def available_actions(s):\n",
" a1 = available_actions_m1(s[0])\n",
" a2 = available_actions_m2(s[1])\n",
" union = set(a1 + a2)\n",
" intersection = set(a1) & set(a2)\n",
" return [x for x in union if x in intersection or x not in SYNC]\n",
"\n",
"def delta(s, a):\n",
" a1 = available_actions_m1(s[0])\n",
" a2 = available_actions_m2(s[1])\n",
" \n",
" if a in a1 and a in a2:\n",
" return prob_product(delta_m1(s[0], a), delta_m2(s[1], a))\n",
" elif a in a1:\n",
" return [(p, (s_, s[1])) for p,s_ in delta_m1(s[0],a)]\n",
" elif a in a2:\n",
" return [(p, (s[0], s_)) for p,s_ in delta_m2(s[1],a)]\n",
" else:\n",
" return [(1,s)]\n",
"\n",
"def labels(s):\n",
" return labels_m1(s[0]) + labels_m2(s[1])\n",
"\n",
"q = pgc.build_pgc(\n",
" initial_state_pgc=((0,0),0),\n",
" available_actions=available_actions,\n",
" labels=labels,\n",
" delta=delta)\n",
"vis_q = show(q)"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "f01f7da3-096d-43e6-94b1-e96a10c8bb5a",
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3 (ipykernel)",
"language": "python",
"name": "python3"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.12.7"
}
},
"nbformat": 4,
"nbformat_minor": 5
}